| Definitions | do-apply(f;x), S  T, X(e), ma-interface-locs(I),  A, A  B, AbsInterface(A), [[I| ]], (x  l),  x:A. B(x), (xL.P(x)), A c B, isl(x),  b, Top, Knd, a:A fp B(a), es-triggers(es;i;ds;conds), t.1, t.2, ma-interface-info(I;i;k), ma-interface-valtype(I;i;k), ma-interface-dom(I;i), ff, tt,   x. t(x), p  q, if b then t else f fi , ma-interface-val(es;X;e), ma-in-interface(es;X;e), ma-interface-ds(I;i), [[X]], [[I|i]], can-apply(f;x), e X,  , {T}, SQType(T), False, P   Q, P & Q, P  Q, t T, P Q, x:A. B(x), X  Y = 0,  , e@i. P(e), ma-interface-consistent2(es;I), Unit, x(s),  , MaInterface(T), a = b, x {FDLNOr12445}, P  Q, Dec(P), fpf-domain(f),  , p-disjoint(A;f;g) |
| Lemmas | outl wf, ma-interface-triggers-list-disjoint, do-apply-p-first-disjoint, l member subtype, l member-set, select wf, length wf1, nat wf, list-set-type, strong-subtype-self, strong-subtype-set3, strong-subtype-deq-subtype, member map, ma-abs-interface-loc, fpf-cap wf, es-vartype wf, member-fpf-dom, pi1 wf, alle-at wf, false wf, fpf-domain wf, es-val wf, es-state-subtype, es-state-when wf, isl wf, not functionality wrt iff, eq id wf, member-fpf-domain, subtype-set-hasloc, subtype rel function, subtype rel set, subtype rel list, subtype rel product, IdLnk wf, fpf-ap wf, es-hasloc, es-kind wf, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, eqtt to assert, bool wf, es-loc wf, top wf, decl-state wf, hasloc wf, Knd wf, fpf wf, fpf-trivial-subtype-top, fpf-dom wf, assert-eq-id, Id sq, ma-interface-triggers-loc, member-remove-repeats, decidable equal Id, decidable l member, l member wf, ma-interface-triggers wf, ma-interface-locs wf, id-deq wf, remove-repeats wf, es-interface wf, Id wf, member map2, es-is-interface-p-first, es-E wf, assert wf, ma-abs-interface wf, ma-interface-triggers-list wf, p-first wf-interface, es-interface-extensionality, es-is-interface wf, ma-interface-consistent-consistent2, event system wf, ma-interface wf, ma-interface-consistent2 wf |